@$i$ (with ds: ${\it ds}$ action $a$:$T$ precondition $a$(v) is $P$ s v)($j$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$if eqof(IdDeq)($j$,$i$)$\rightarrow$ (with ds: ${\it ds}$ action $a$:$T$ precondition $a$(v) is $P$ s v) else  fi